$\forall$${\it ds}$:(Id$\rightarrow$Type), ${\it da}$:(Id$\rightarrow$Knd$\rightarrow$Type), $A$:Type, $X$:Interface(${\it ds}$;${\it da}$;$A$), ${\it es}$:ES, $e$:E.
\\[0ex]es{-}decl(${\it es}$;${\it ds}$;${\it da}$) $\Rightarrow$ (in{-}interface(${\it es}$;$X$;$e$) $\in$ $\mathbb{B}$)